Consider the TRS R consisting of the rewrite rules
1:
minus(x,0)
→ x
2:
minus(s(x),s(y))
→ minus(x,y)
3:
quot(0,s(y))
→ 0
4:
quot(s(x),s(y))
→ s(quot(minus(x,y),s(y)))
There are 3 dependency pairs:
5:
MINUS(s(x),s(y))
→ MINUS(x,y)
6:
QUOT(s(x),s(y))
→ QUOT(minus(x,y),s(y))
7:
QUOT(s(x),s(y))
→ MINUS(x,y)
The approximated dependency graph contains 2 SCCs:
{5}
and {6}.
Consider the SCC {5}.
There are no usable rules.
By taking the AF π with
π(MINUS) = 1 together with
the lexicographic path order with
empty precedence,
rule 5
is strictly decreasing.
Consider the SCC {6}.
The usable rules are {1,2}.
By taking the AF π with
π(minus) = π(QUOT) = 1 together with
the lexicographic path order with
empty precedence,
rule 1
is weakly decreasing and
the rules in {2,6}
are strictly decreasing.